Search Results

Documents authored by Hermanns, Holger

Document
Invited Paper
DOI: 10.4230/LIPIcs.CONCUR.2020.5
CONCUR Test-Of-Time Award 2020 Announcement (Invited Paper)

Authors: Luca Aceto, Jos Baeten, Patricia Bouyer-Decitre, Holger Hermanns, and Alexandra Silva

Published in: LIPIcs, Volume 171, 31st International Conference on Concurrency Theory (CONCUR 2020)

Abstract
This short article announces the recipients of the CONCUR Test-of-Time Award 2020.
Cite as

Luca Aceto, Jos Baeten, Patricia Bouyer-Decitre, Holger Hermanns, and Alexandra Silva. CONCUR Test-Of-Time Award 2020 Announcement (Invited Paper). In 31st International Conference on Concurrency Theory (CONCUR 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 171, pp. 5:1-5:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{aceto_et_al:LIPIcs.CONCUR.2020.5,
  author =	{Aceto, Luca and Baeten, Jos and Bouyer-Decitre, Patricia and Hermanns, Holger and Silva, Alexandra},
  title =	{{CONCUR Test-Of-Time Award 2020 Announcement}},
  booktitle =	{31st International Conference on Concurrency Theory (CONCUR 2020)},
  pages =	{5:1--5:3},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-160-3},
  ISSN =	{1868-8969},
  year =	{2020},
  volume =	{171},
  editor =	{Konnov, Igor and Kov\'{a}cs, Laura},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2020.5},
  URN =		{urn:nbn:de:0030-drops-128172},
  doi =		{10.4230/LIPIcs.CONCUR.2020.5},
  annote =	{Keywords: Concurrency, CONCUR Test-of-Time Award}
}
Document
DOI: 10.4230/LITES-v004-i001-a004
How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty

Authors: Holger Hermanns, Jan Krčál, and Gilles Nies

Published in: LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1

Abstract
The kinetic battery model is a popular model of the dynamic behaviour of a conventional battery, useful to predict or optimize the time until battery depletion. The model however lacks certain obvious aspects of batteries in-the-wild, especially with respect to the effects of random influences and the behaviour when charging up to capacity limits.This paper considers the kinetic battery model with limited capacity in the context of piecewise constant yet random charging and discharging. We provide exact representations of the battery behaviour wherever possible, and otherwise develop safe approximations that bound the probability distribution of the battery state from above and below. The resulting model enables the time-dependent evaluation of the risk of battery depletion. This is demonstrated in an extensive dependability study of a nano satellite currently orbiting the earth.
Cite as

Holger Hermanns, Jan Krčál, and Gilles Nies. How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty. In LITES, Volume 4, Issue 1 (2017). Leibniz Transactions on Embedded Systems, Volume 4, Issue 1, pp. 04:1-04:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{hermanns_et_al:LITES-v004-i001-a004,
  author =	{Hermanns, Holger and Kr\v{c}\'{a}l, Jan and Nies, Gilles},
  title =	{{How Is Your Satellite Doing? Battery Kinetics with Recharging and Uncertainty}},
  journal =	{Leibniz Transactions on Embedded Systems},
  pages =	{04:1--04:28},
  ISSN =	{2199-2002},
  year =	{2017},
  volume =	{4},
  number =	{1},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LITES-v004-i001-a004},
  doi =		{10.4230/LITES-v004-i001-a004},
  annote =	{Keywords: Battery Power, Depletion Risk, Bounded Charging and Discharging, Stochastic Load, Distribution Bounds}
}
Document
Invited Talk
DOI: 10.4230/LIPIcs.FSTTCS.2016.3
My O Is Bigger Than Yours (Invited Talk)

Authors: Holger Hermanns

Published in: LIPIcs, Volume 65, 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)

Abstract
This invited talk starts off with a review of probabilistic safety assessment (PSA) methods currently exercised across the nuclear power plant domain worldwide. It then elaborates on crucial aspects of the Fukushima Dai-ichi accident which are not considered properly in contemporary PSA studies. New kinds of PSA are needed so as to take into account external hazards, dynamic aspects of accident progression, and partial information. All of these come with obvious increases in algorithmic analysis complexity. This motivates our ongoing work to gradually tackle the resulting modelling and analysis problems. They revolve around static and dynamic fault trees, open interpretations of compositional Markov models and advances in their effective numerical analysis.
Cite as

Holger Hermanns. My O Is Bigger Than Yours (Invited Talk). In 36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 65, pp. 3:1-3:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016)

Copy BibTex To Clipboard

@InProceedings{hermanns:LIPIcs.FSTTCS.2016.3,
  author =	{Hermanns, Holger},
  title =	{{My O Is Bigger Than Yours}},
  booktitle =	{36th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2016)},
  pages =	{3:1--3:2},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-027-9},
  ISSN =	{1868-8969},
  year =	{2016},
  volume =	{65},
  editor =	{Lal, Akash and Akshay, S. and Saurabh, Saket and Sen, Sandeep},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2016.3},
  URN =		{urn:nbn:de:0030-drops-68881},
  doi =		{10.4230/LIPIcs.FSTTCS.2016.3},
  annote =	{Keywords: Probabilistic Safety Analysis, Fault Trees, Compositionality, Markov Models, Model Checking}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.435
Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time

Authors: Holger Hermanns and Andrea Turrini

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
Deciding in an efficient way weak probabilistic bisimulation in the context of probabilistic automata is an open problem for about a decade. In this work we close this problem by proposing a procedure that checks in polynomial time the existence of a weak combined transition satisfying the step condition of the bisimulation. This enables us to arrive at a polynomial time algorithm for deciding weak probabilistic bisimulation. We also present several extensions to interesting related problems setting the ground for the development of more effective and compositional analysis algorithms for probabilistic systems.
Cite as

Holger Hermanns and Andrea Turrini. Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 435-447, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{hermanns_et_al:LIPIcs.FSTTCS.2012.435,
  author =	{Hermanns, Holger and Turrini, Andrea},
  title =	{{Deciding Probabilistic Automata Weak Bisimulation in Polynomial Time}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{435--447},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.435},
  URN =		{urn:nbn:de:0030-drops-38794},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.435},
  annote =	{Keywords: Probabilistic Automata, Weak probabilsitic bisimulation, Linear Programming problem, Polynomial decision algorithm}
}
Document
DOI: 10.4230/LIPIcs.FSTTCS.2012.474
Verification of Open Interactive Markov Chains

Authors: Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak

Published in: LIPIcs, Volume 18, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)

Abstract
Interactive Markov chains (IMC) are compositional behavioral models extending both labeled transition systems and continuous-time Markov chains. IMC pair modeling convenience - owed to compositionality properties - with effective verification algorithms and tools - owed to Markov properties. Thus far however, IMC verification did not consider compositionality properties, but considered closed systems. This paper discusses the evaluation of IMC in an open and thus compositional interpretation. For this we embed the IMC into a game that is played with the environment. We devise algorithms that enable us to derive bounds on reachability probabilities that are assured to hold in any composition context.
Cite as

Tomas Brazdil, Holger Hermanns, Jan Krcal, Jan Kretinsky, and Vojtech Rehak. Verification of Open Interactive Markov Chains. In IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012). Leibniz International Proceedings in Informatics (LIPIcs), Volume 18, pp. 474-485, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2012)

Copy BibTex To Clipboard

@InProceedings{brazdil_et_al:LIPIcs.FSTTCS.2012.474,
  author =	{Brazdil, Tomas and Hermanns, Holger and Krcal, Jan and Kretinsky, Jan and Rehak, Vojtech},
  title =	{{Verification of Open Interactive Markov Chains}},
  booktitle =	{IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2012)},
  pages =	{474--485},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-939897-47-7},
  ISSN =	{1868-8969},
  year =	{2012},
  volume =	{18},
  editor =	{D'Souza, Deepak and Radhakrishnan, Jaikumar and Telikepalli, Kavitha},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/LIPIcs.FSTTCS.2012.474},
  URN =		{urn:nbn:de:0030-drops-38826},
  doi =		{10.4230/LIPIcs.FSTTCS.2012.474},
  annote =	{Keywords: IMC, compositional verification, synthesis, time bounded reachability, discretization}
}
Document
DOI: 10.4230/DagRep.1.1.1
Multi-Core Memory Models and Concurrency Theory (Dagstuhl Seminar 11011)

Authors: Hans J. Boehm, Ursula Goltz, Holger Hermanns, and Peter Sewell

Published in: Dagstuhl Reports, Volume 1, Issue 1 (2011)

Abstract
This report documents the programme and the outcomes of Dagstuhl Seminar 11011 "Multi-Core Memory Models and Concurrency Theory".
Cite as

Hans J. Boehm, Ursula Goltz, Holger Hermanns, and Peter Sewell. Multi-Core Memory Models and Concurrency Theory (Dagstuhl Seminar 11011). In Dagstuhl Reports, Volume 1, Issue 1, pp. 1-26, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2011)

Copy BibTex To Clipboard

@Article{boehm_et_al:DagRep.1.1.1,
  author =	{Boehm, Hans J. and Goltz, Ursula and Hermanns, Holger and Sewell, Peter},
  title =	{{Multi-Core Memory Models and Concurrency Theory (Dagstuhl Seminar 11011)}},
  pages =	{1--26},
  journal =	{Dagstuhl Reports},
  ISSN =	{2192-5283},
  year =	{2011},
  volume =	{1},
  number =	{1},
  editor =	{Boehm, Hans J. and Goltz, Ursula and Hermanns, Holger and Sewell, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagRep.1.1.1},
  URN =		{urn:nbn:de:0030-drops-31058},
  doi =		{10.4230/DagRep.1.1.1},
  annote =	{Keywords: Relaxed Memory Models, Concurrency Theory, Multi-Core, Semantics, Parallel Programming, Cache Coherence}
}
Document
DOI: 10.4230/DagSemProc.10271.1
10271 Abstracts Collection – Verification over discrete-continuous boundaries

Authors: Bernd Becker, Luca Cardelli, Holger Hermanns, and Sofiene Tahar

Published in: Dagstuhl Seminar Proceedings, Volume 10271, Verification over discrete-continuous boundaries (2010)

Abstract
From 4 July 2010 to 9 July 2010, the Dagstuhl Seminar 10271 ``Verification over discrete-continuous boundaries'' was held in Schloss Dagstuhl~--~Leibniz Center for Informatics. During the seminar, several participants presented their current research, and ongoing work and open problems were discussed. Abstracts of the presentations given during the seminar as well as abstracts of seminar results and ideas are put together in this paper. The first section describes the seminar topics and goals in general. Links to extended abstracts or full papers are provided, if available.
Cite as

Bernd Becker, Luca Cardelli, Holger Hermanns, and Sofiene Tahar. 10271 Abstracts Collection – Verification over discrete-continuous boundaries. In Verification over discrete-continuous boundaries. Dagstuhl Seminar Proceedings, Volume 10271, pp. 1-19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2010)

Copy BibTex To Clipboard

@InProceedings{becker_et_al:DagSemProc.10271.1,
  author =	{Becker, Bernd and Cardelli, Luca and Hermanns, Holger and Tahar, Sofiene},
  title =	{{10271 Abstracts Collection – Verification over discrete-continuous boundaries}},
  booktitle =	{Verification over discrete-continuous boundaries},
  pages =	{1--19},
  series =	{Dagstuhl Seminar Proceedings (DagSemProc)},
  ISSN =	{1862-4405},
  year =	{2010},
  volume =	{10271},
  editor =	{Bernd Becker and Luca Cardelli and Holger Hermanns and Sofiene Tahar},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops-dev.dagstuhl.de/entities/document/10.4230/DagSemProc.10271.1},
  URN =		{urn:nbn:de:0030-drops-27922},
  doi =		{10.4230/DagSemProc.10271.1},
  annote =	{Keywords: Formal verification, cyber-physical systems, analog circuits, theorem proving, systems biology, mean-field methods}
}
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact